Nuprl Lemma : upto_is_nil
11,40
postcript
pdf
n
:
. (upto(
n
) = []
(
List))
(
n
= 0
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
t
T
,
,
S
T
,
||
as
||
,
Y
,
,
upto(
n
)
,
if
b
then
t
else
f
fi
,
(
i
=
j
)
,
tt
,
A
B
,
A
,
False
,
{
i
..
j
}
Lemmas
upto
wf
,
int
seg
wf
,
nat
wf
,
length
wf1
,
length
upto
,
le
wf
origin
n:
. (upto(n) = [] 
(
List)) 
(n = 0 ) n:. (upto(n) = [] ( List)) (n = 0 ) x:A. B(x) Q Q Q T
T
j)
B
A
}